the_es:ES, T:Type, f:(IdT), g:(IdLnkIdT), e:E.
case(kind(e))act(a) => f(a)rcv(l,tg) => g(l,tg)  T 

latex

Definitions	E, IdLnk, Id, ES, case(kind(e))act(a) => f(a)rcv(l,tg) => g(l;tg), Unit, P  Q, P & Q, isrcv(e), x(s1,s2), lnk(e), tag(e), , Prop, b, A, b, x(s), t  T, act(e), x:A. B(x), P  Q
Lemmas	es-act wf, assert wf, not wf, bnot wf, es-tag wf, es-lnk wf, bool wf, es-isrcv wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, Id wf, IdLnk wf, es-E wf